翻訳と辞書 Words near each other ・ Harrold (surname) ・ Harrold Airport ・ Harrold Brothers ・ Harrold Hall ・ Harrold Independent School District ・ Harrold Municipal Airport ・ Harrold Priory ・ Harrold Priory Middle School ・ Harrold, Bedfordshire ・ Harrold, South Dakota ・ Harrold, Texas ・ Harrold-Odell Country Park ・ Harron ・ Harrop ・ Harrop Fold School ・ Harrop formula ・ Harrop Island ・ Harroun ・ Harrow ・ Harrow & Wealdstone station ・ Harrow (surname) ・ Harrow (tool) ・ Harrow (UK Parliament constituency) ・ Harrow Airport ・ Harrow and Uxbridge Railway ・ Harrow and Uxbridge Railway Act 1897 ・ Harrow and Wealdstone rail crash ・ Harrow Arts Centre ・ Harrow Borough F.C. ・ Harrow bus station Dictionary Lists mini英和辞書 mini和英辞書 Webster 1913 Latin-English FOLDOC Wikipedia English ウィキペディア

翻訳と辞書　辞書検索 [ 開発暫定版 ] スポンサード リンク Harrop formula ： ウィキペディア英語版 Harrop formula In intuitionistic logic, the Harrop formulae, named after Ronald Harrop, are the class of formulae inductively defined as follows: * Atomic formulae are Harrop, including falsity (⊥); * $A\; \backslash wedge\; B$ is Harrop provided $A$ and $B$ are; * $\backslash neg\; F$ is Harrop for any well-formed formula $F$; * $F\; \backslash rightarrow\; A$ is Harrop provided $A$ is, and $F$ is any well-formed formula; * $\backslash forall\; x.\; A$ is Harrop provided $A$ is. By excluding disjunction and existential quantification (except in the antecedent of implication), non-constructive predicates are avoided, which has benefits for computer implementation. From a constructivist point of view, Harrop formulae are "well-behaved." For example, in Heyting arithmetic, Harrop formulae satisfy a classical equivalence not usually satisfied in constructive logic:〔 : $A\; \backslash leftrightarrow\; \backslash neg\; \backslash neg\; A.$ Harrop formulae were introduced around 1956 by Ronald Harrop and independently by Helena Rasiowa.〔 Variations of the fundamental concept are used in different branches of constructive mathematics and logic programming. ==Hereditary Harrop formulae and logic programming== A more complex definition of hereditary Harrop formulae is used in logic programming as a generalisation of horn clauses, and forms the basis for the language λProlog. Hereditary Harrop formulae are defined in terms of two (sometimes three) recursive sets of formulae. In one formulation:〔Dov M. Gabbay, Christopher John Hogger, John Alan Robinson, ''Handbook of Logic in Artificial Intelligence and Logic Programming: Logic programming'', Oxford University Press, 1998, p 575, ISBN 0-19-853792-1〕 * Rigid atomic formulae, i.e. constants $r$ or formulae $r(t\_1,...,t\_n)$, are hereditary Harrop; * $A\; \backslash wedge\; B$ is hereditary Harrop provided $A$ and $B$ are; * $\backslash forall\; x.\; A$ is hereditary Harrop provided $A$ is; * $G\; \backslash rightarrow\; A$ is hereditary Harrop provided $A$ is rigidly atomic, and $G$ is a ''G''-formula. ''G''-formulae are defined as follows:〔 * Atomic formulae are ''G''-formulae, including truth(⊤); * $A\; \backslash wedge\; B$ is a ''G''-formula provided $A$ and $B$ are; * $A\; \backslash vee\; B$ is a ''G''-formula provided $A$ and $B$ are; * $\backslash forall\; x.\; A$ is a ''G''-formula provided $A$ is; * $\backslash exists\; x.\; A$ is a ''G''-formula provided $A$ is; * $H\; \backslash rightarrow\; A$ is a ''G''-formula provided $A$ is, and $H$ is hereditary Harrop. 抄文引用元・出典: フリー百科事典『 ウィキペディア（Wikipedia）』 ■ウィキペディアで「Harrop formula」の詳細全文を読む スポンサード リンク 翻訳と辞書 : 翻訳のためのインターネットリソース Copyright(C) kotoba.ne.jp 1997-2016. All Rights Reserved.